/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking;

import caetus.modelChecking.goal.ModelGoal;
import caetus.modelChecking.goal.ModelGoalMap;
import caetus.modelChecking.role.ModelActor;
import caetus.modelChecking.role.ModelEnvironment;
import caetus.modelChecking.role.ModelPerson;
import caetus.modelChecking.role.ModelSession;
import caetus.modelChecking.role.ModelToken;
import caetus.modelChecking.variable.ModelBaseVariable;
import caetus.modelChecking.variable.ModelConstants;
import caetus.modelChecking.variable.ModelVariable;
import caetus.modelChecking.variable.ModelVariableType;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import caetus.pkcs11.tokenCapabilities.TokenCapability;
import caetus.pkcs11.tokenCapabilities.TokenCapabilityGroup;
import caetus.pkcs11.tokenCapabilities.TokenCapabilityValue;
import java.util.LinkedList;
import java.util.List;

/**
 * This class takes the capabilities of the token and converts them into a hlpsl
 * file that is later given to the model checker. This version should work with
 * both cl-atse and satmc. The models created this way are stateless, but if
 * ever relevant, it is fully possible to make a state-based model.
 *
 * @author Josef Hertl
 */
public class ModelMaker {

    private TokenCapabilities tokenCapabilities;

    public ModelMaker(TokenCapabilities tokenCapabilities) {
        this.tokenCapabilities = tokenCapabilities;
    }

    /**
     * Completely prepares a model that can be passed over to the model-checker.
     *
     * @return String form of the model.
     */
    public String prepareModel() {
        ModelVariable TA = new ModelBaseVariable("TA", ModelVariableType.AGENT);
        ModelVariable E = new ModelBaseVariable("E", ModelVariableType.AGENT);
        List<ModelVariable> agentList = new LinkedList<ModelVariable>();
        agentList.add(TA);
        agentList.add(E);

        ModelToken tokenA = new ModelToken(TA, "tokenA", tokenCapabilities);
        tokenA.addToGlobalVariables(agentList);
        ModelPerson eve = new ModelPerson(E, "eve", tokenCapabilities);
        eve.addToGlobalVariables(agentList);

        List<ModelActor> tokenList = new LinkedList<ModelActor>();
        tokenList.add(tokenA);
        ModelGoalMap.setActorList(tokenList);

        ModelSession session = new ModelSession(tokenCapabilities);
        session.addToGlobalVariables(agentList);

        ModelEnvironment environment = new ModelEnvironment(session, tokenCapabilities);

        if (tokenCapabilities.capabilityWorking(TokenCapability.OBVIOUS_WEAKNESS)) {
            //enables the weakness - to show that the token can find the attack
            ModelConstants.add(new ModelBaseVariable("show_weakness", ModelVariableType.TEXT));
        }
        if (tokenCapabilities.capabilityGroupWorking(TokenCapabilityGroup.SYMMETRIC_CRYPTOGRAPHY)) {
            ModelBaseVariable SK = new ModelBaseVariable("SK", ModelVariableType.SYMMETRIC_KEY); //the pre-shared symmetric key
            for (ModelActor modelToken : tokenList) {
                modelToken.addGlobalVariable(SK);
            }
            session.addGlobalVariable(SK);
            if (tokenCapabilities.capabilityWorking(TokenCapability.CREATE_SYMMETRIC)) {
                ModelBaseVariable ISK = new ModelBaseVariable("ISK", ModelVariableType.SYMMETRIC_KEY);//the imported key, Eve knows it
                for (ModelActor modelToken : tokenList) {
                    modelToken.addGlobalVariable(ISK);
                }
                session.addGlobalVariable(ISK);
                eve.addGlobalVariable(ISK);
            }
        }
        if (tokenCapabilities.capabilityGroupWorking(TokenCapabilityGroup.ASYMMETRIC_CRYPTOGRAPHY)) {
            ModelBaseVariable PuK = new ModelBaseVariable("PuK", ModelVariableType.PUBLIC_KEY);//preshared public key
            ModelBaseVariable PrK = new ModelBaseVariable("PrK", ModelVariableType.PRIVATE_KEY);//preshared private key
            for (ModelActor modelToken : tokenList) {
                modelToken.addGlobalVariable(PuK);
                modelToken.addGlobalVariable(PrK);
            }
            eve.addGlobalVariable(PuK);
            session.addGlobalVariable(PuK);
            session.addLocalVariable(PrK); //private key is added as a local variable of the session and later generated in its init
            if (tokenCapabilities.capabilityWorking(TokenCapability.ASYMMETRIC_KEY_GENERATION)) {
                ModelConstants.add(new ModelBaseVariable("generate_asymmetric", ModelVariableType.TEXT));
            }
            if (tokenCapabilities.capabilityWorking(TokenCapability.CREATE_ASYMMETRIC)) {
                ModelConstants.add(new ModelBaseVariable("create_asymmetric", ModelVariableType.TEXT));
            }
        }
        if (tokenCapabilities.capabilityGroupWorking(TokenCapabilityGroup.WRAPPING_KEYS)) {
            ModelConstants.add(new ModelBaseVariable("unwrap_success", ModelVariableType.TEXT));
        }
        if (tokenCapabilities.capabilityWorking(TokenCapability.WRAPPING_SYMMETRIC_BY_SYMMETRIC)) {
            //this wrapping signal also includes sending the key
            ModelConstants.add(new ModelBaseVariable("wrap_secret_by_secret", ModelVariableType.TEXT));
        }
        if (tokenCapabilities.capabilityWorking(TokenCapability.WRAPPING_SYMMETRIC_BY_ASYMMETRIC)) {
            //this wrapping signal also includes sending the key
            ModelConstants.add(new ModelBaseVariable("wrap_secret_by_public", ModelVariableType.TEXT));
        }
        if (tokenCapabilities.capabilityWorking(TokenCapability.WRAPPING_ASYMMETRIC_BY_SYMMETRIC)) {
            //this wrapping signal also includes sending the key
            ModelConstants.add(new ModelBaseVariable("wrap_private_by_secret", ModelVariableType.TEXT));
        }
        if (tokenCapabilities.capabilityWorking(TokenCapability.WRAPPING_ASYMMETRIC_BY_ASYMMETRIC)) {
            //this wrapping signal also includes sending the key
            ModelConstants.add(new ModelBaseVariable("wrap_private_by_private", ModelVariableType.TEXT));
        }

        for (ModelActor modelToken : tokenList) {
            session.addChannelsFromActor(modelToken, modelToken.generateChannels());
        }
        session.addChannelsFromActor(eve, eve.generateChannels());

        for (ModelActor modelToken : tokenList) {
            modelToken.generateLocalVariables();
        }
        eve.generateLocalVariables();

        ModelGoal goal = new ModelGoal();

        String model = "";
        for (ModelActor modelToken : tokenList) {
            model += modelToken.makeRole();
        }
        model += eve.makeRole();
        model += session.makeRole();
        model += environment.makeRole();
        model += goal.makeGoal();
        model += "\nenvironment()\n";
        return model;
    }
}
